Nuprl Lemma : msg-spec-links-spec1
11,40
postcript
pdf
l
,
k
,
tg
,
f
,
n
:Top. msg-spec-links(
k
sends on
l
with tag
tg
[
s
,
v
.
f
(
s
,
v
)], at marker
n
) ~ [
l
]
latex
Definitions
k
sends on
l
with tag
tg
[
s
,
v
.
f
(
s
;
v
)], at marker
n
,
msg-spec-links(
snd
)
,
x
:
A
.
B
(
x
)
,
t
T
,
Top
Lemmas
top
wf
origin
l, k, tg, f, n:Top. msg-spec-links(k sends on l with tag tg [s,v.f(s,v)], at marker n) ~ [l] l, k, tg, f, n:Top. msg-spec-links(k sends on l with tag tg [s,v.f(s,v)], at marker n) ~ [l] x:A. B(x)
T